r:, n:. r  n   

latex

Definitions	t.1, |r|, <+*>, r  n, t  T, x:A. B(x), CRng, Rng
Lemmas	rationals wf, nat wf, rng car wf, crng wf, qrng wf, rng nexp wf